\subsection{表决协议}
尽管提名过程会继续更新合成值，一旦节点有了合成值它们将参与表决协议。一个表决$b$是一个形如$b=\langle n,x\rangle$的二元组，这里$x\neq \perp$是一个值，而$b$是对当前{\slot}具体化的公决(referendum)。$n\geq 1$是一个用于确保大的表决数总可访问的计数器。我们使用类C语言的标记$b.n$和$b.x$来表示表决$b$的计数和合成值的域，因而有$b=\langle b.n, b.x\rangle$。表决是全序的，且$b.n$比$b.x$更为重要{\footnote{译注：指二元组$b_1\preceq b_2$当且仅当1) $b_1.n \leq b_2.n$；或2) $b_1.n=b_2.n \wedge b_1.x \leq b_2.x$。}}。为了方便起见，一个特殊的无效空表决$\mybm{0}=\langle 0,\perp\rangle$小于其它任何表决，而一个特别的计数器$\infty$大于其它所有计数器。

我们分别用``提交表决$b$''或``终止表决$b$''分别代称使用联邦选举来对语句$commib\;b$和$abort\;b$进行认可。对于给定的表决，$commit$和$abort$是相互冲突的，因此一个良性行为的节点最多投票赞成两者之一。在第\ref{sec:voting}节的标注系统下，$commit\;b$的反是$\overline{commit\;b}$，但使用$abort\;b$更为直观。

由于对某个{\slot}至多只有一个值被选用，所有提交的和被卡住的表决必须包含相同的值。粗略地说，这意味着如果\textit{提交类}陈述和更小的非终止表决相冲突的话那么它是无效的。

\begin{definition}[相容的]
        两个表决是\textbf{相容的}(记作$b_1 \sim b_2$)当且仅当$b_1.x=b_2.x$；它们是\textbf{不相容的}(记作$b_1\not\sim b_2$)当且仅当$b_1.x\neq b_2.x$。我们还将$b_1\leq b_2$(或等价地，$b_2\geq b_1$)且$b_1\sim b_2$记作$b_1\lesssim b_2$($b_2\gtrsim b_1$)。类似地，$b_1\lnsim b_2$或$b_2\gnsim b_1$意味着$b_1\leq b_2$(或等价地$b_2\geq \b_1$)且$b_1\not\sim b_2$。
\end{definition}

\begin{definition}[就绪的]
        一个表决$b$是\textbf{就绪的}当且仅当下面集合中的每个陈述都为真：$\left\{abort\;b_{old}|b_{old}\lnsim b\right\}$。
\end{definition}

更准确地说，如果$b$被确认是就绪的，那么$commit\;b$对投赞成票来说是有效的，节点通过对应的$abort$陈述的联邦选举保障它。全体一致地对这些陈述进行投票是方便的，因此不论我们在哪里认定{\todo{使用准确表述}}``$b$就绪''，周围的环境将应用于$abort$陈述的整个集合中。特别地，一个节点投票赞成、接受或确认$b$就绪当且仅当它分别投票赞成、接受或确认它们全部\textit{终止}了。

为了提交一个表决并向外界展示它的值$b.x$，SCP节点首先接受并确认$b$已经就绪，然后接受并确认$commit\;b$。在第一个完好节点投票赞成$commit\;b$之前，经由联邦投票的准备步骤确保所有完好节点最终可以确认$b$是就绪的。当一个完好节点$v$接受$commit\;b$时，意味着$b.x$最终将会被选中。然而，正如第\ref{sec:voting_safety}中所讨论的那样，为了防止$v$被污染，$v$必须在作用于它之前确认\textit{提交类}陈述。

\input{tex/6-scp-s2-1}
\input{tex/6-scp-s2-2}